package model.cnf;

/**
 * Represent a CNF that is store in memory. Be aware that some CNF can be really big so MemoryCNF will take even memory to be store, so only use them when you need to do a lot of I/O operation on it unless use FileCNF for a minimal use of memory.
 */
import java.io.BufferedReader;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.List;
import java.util.Scanner;



public class MemoryCNF extends CNF {

	protected List<Clause> clauses = new ArrayList<Clause>();
	
	
	public MemoryCNF(String CNFfile) throws Exception{
		this.CNFfile = new File(CNFfile);
		
		check();
	}

	/**
	 * get all the data from the CNF file and store them in memory
	 * @throws Exception
	 */
	private void putInMemory() throws IOException{
		clauses=new ArrayList<Clause>();	

		BufferedReader br = null;
		try{
			InputStream in = new FileInputStream(CNFfile);	

			InputStreamReader ipsr=new InputStreamReader(in);
			br = new BufferedReader(ipsr);

			String line;
			while ((line = br.readLine()) != null)
			{//lit la CNF
				int i;
				//System.out.println("lit une ligne");
				if(line.charAt(0) == COMMENTAIRE) 
					continue;
				if(line.charAt(0) == DESCRIPTION)
				{
					Scanner sc = new Scanner(line.substring(SIZE_DESCRIPTION));
					declaredNumVar = sc.nextInt();
					declaredNumClause = sc.nextInt();
					continue;
				}

				List<Literal> c = new ArrayList<Literal>();
				Scanner sc=new Scanner(line);
				while((i = sc.nextInt()) != 0){
					c.add(new Literal(i));
				}

				addClause(c);
			}
		}
		catch(IOException e){
			e.printStackTrace();
			throw e;
		}
		finally{
			if(br != null)
				br.close();
		}
	}


	public String toString(){
		StringBuffer s=new StringBuffer();
		s.append("p cnf ");
		s.append(String.valueOf(declaredNumVar));
		s.append(" ");
		s.append(String.valueOf(declaredNumClause));
		s.append("\n");
		for(Clause cl : clauses){
			s.append(cl.toString());
			s.append("0\n");
		}
		return s.toString();
	}
	
	@Override
	public File export(String cnf, File directory) {
		// TODO verifier les nom et s'occuper des execption
	
		File res = new File(directory, cnf);
		FileWriter fw = null;
		
		try {
			res.createNewFile();
			
			fw = new FileWriter(res);
			fw.write(toString());
		
		} catch (IOException e) {
			e.printStackTrace();
			
			res.delete();
			res = null;
		}
		finally{
			try {
				if( fw != null)
					fw.close();
			} catch (IOException e) {
				e.printStackTrace();
			}
		}
		
		if(res != null)
			modify = false;
		
		return res;
	}

	@Override
	public File export(File directory) {
		String name;
		try {
			System.out.println("prefix "+PREFIX+getFileName()+" suffix "+ SUFFIX);
			name = File.createTempFile(PREFIX+getFileName(), SUFFIX, directory).getName();
		} catch (IOException e) {
			e.printStackTrace();
			
			return null;
		}
		return export(name, directory);
	}

	
	public int size(){
		return clauses.size();	
	}
	
	
	@Override
	public void check() throws Exception {
		putInMemory();
		
		stat = new Stat(this);
		
		modify = false;
	}

	@Override
	public List<Clause> getClauses() throws Exception {
		return clauses;
	}

	@Override
	public void addClause(List<Literal> cl) {
		if(cl.isEmpty())
			return;
		
		modify = true;
		clauses.add(new Clause(cl));
	}

	@Override
	public void addClause(Clause cl) {
		modify = true;
		clauses.add(cl);
	}

	@Override
	public Clause getClause(int i) {
		return clauses.get(i);
	}

	@Override
	public void checkStat() throws Exception{
		this.stat = new Stat(this);
	}

}
